(declare-sort S0 0)

(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const i0 Int)
(declare-const arr-8105523187944350698_752445606576065925-0 (Array Bool Int))
(declare-const arr-8105523187944350698_912377959025502099-0 (Array Bool (Array Bool Int)))
(declare-const arr--6035557599497917479_8105523187944350698-0 (Array (Array Bool (Array Bool Int)) Bool))
(declare-const v14 Bool)
(declare-const arr--6035557599497917479_8105523187944350698-1 (Array (Array Bool (Array Bool Int)) Bool))
(declare-const arr-8105523187944350698_-6035557599497917479-0 (Array Bool (Array Bool (Array Bool Int))))
(declare-const v17 Bool)
(declare-const arr--6035557599497917479_1184966662324556901-0 (Array (Array Bool (Array Bool Int)) (Array (Array Bool (Array Bool Int)) Bool)))
(declare-const v18 Bool)
(declare-const i3 Int)
(declare-const arr-8105523187944350698_3740047279165590495-0 (Array Bool (Array Bool (Array Bool (Array Bool Int)))))
(declare-const arr-1184966662324556901_-6035557599497917479-0 (Array (Array (Array Bool (Array Bool Int)) Bool) (Array Bool (Array Bool Int))))
(declare-const arr-912377959025502099_8105523187944350698-0 (Array (Array Bool Int) Bool))
(declare-const i4 Int)
(assert (or (not (>= 6 i0))))
(assert (or v17 (= arr-8105523187944350698_912377959025502099-0 (store arr-8105523187944350698_912377959025502099-0 v14 (store arr-8105523187944350698_752445606576065925-0 (=> v3 v4) 6)) (store arr-8105523187944350698_912377959025502099-0 v14 (store arr-8105523187944350698_752445606576065925-0 (=> v3 v4) 6)) arr-8105523187944350698_912377959025502099-0) v18 (or v2 (=> v3 v4))))
(check-sat)
